Nuprl Lemma : qdiv-self
11,40
postcript
pdf
r
:
. (
(
r
= 0
))
((
r
/
r
) = 1
)
latex
Definitions
,
t
T
,
(
r
/
s
)
,
P
Q
,
x
:
A
.
B
(
x
)
,
S
T
Lemmas
qmul
inv
,
int
inc
rationals
,
rationals
wf
,
not
wf
origin
r:
. (
(r = 0 
)) 
((r/r) = 1 ) r:. ((r = 0 )) ((r/r) = 1 ) 
T Qx:A. B(x)
T